package list3;

public class ListIterImpl implements ListIter {
	/*@ readonly @*/ List thelist;
	/*@ readonly @*/ Entry cur;
	
	/*@ pure @*/
	public ListIterImpl(/*@ readonly @*/ List list) {
		thelist = list;
		cur = list.first;
	}
	
	/*@ pure @*/
	public /*@ readonly @*/ Object getCurrent() {
		return cur != null ? cur.data : null;
	}
	
	public void next() {
		if (cur != null) {
			cur = cur.next;
		}
	}

	/*@ pure @*/
	public boolean hasCurrent() {
		return cur != null;
	}
	
	//@ also requires getList() instanceof peer List;
	public void remove() {
		if( thelist instanceof /*@ peer @*/ List) {
			// if the precondition is respected, this cast will work
			((/*@ peer @*/ List) thelist).remove(cur);
		} else {
			// if the precondition was not checked and the list is not
			// modifiable, we throw an exception
			throw new java.lang.UnsupportedOperationException();
		}
	}

	/*@ pure @*/
	public /*@ readonly @*/ List getList() {
		return thelist;
	}	
}
